Nuprl Definition : dec_binrel
13,42
postcript
pdf
dec_binrel(
T
;
r
) ==
x
,
y
:
T
. Dec(
r
(
x
,
y
))
latex
clarification:
dec_binrel(
T
;
r
) ==
x
:
T
,
y
:
T
. Dec(
r
(
x
,
y
))
latex
Up
gen
algebra
1
Wellformedness Lemmas
dec
binrel
wf
Definitions
x
:
A
.
B
(
x
)
,
Dec(
P
)
origin
x, y:T. Dec(r(x,y))
x:T, y:T. Dec(r(x,y)) x, y:T. Dec(r(x,y))
x:T, y:T. Dec(r(x,y)) x:A. B(x)